Problem:
 rec(rec(x)) -> sent(rec(x))
 rec(sent(x)) -> sent(rec(x))
 rec(no(x)) -> sent(rec(x))
 rec(bot()) -> up(sent(bot()))
 rec(up(x)) -> up(rec(x))
 sent(up(x)) -> up(sent(x))
 no(up(x)) -> up(no(x))
 top(rec(up(x))) -> top(check(rec(x)))
 top(sent(up(x))) -> top(check(rec(x)))
 top(no(up(x))) -> top(check(rec(x)))
 check(up(x)) -> up(check(x))
 check(sent(x)) -> sent(check(x))
 check(rec(x)) -> rec(check(x))
 check(no(x)) -> no(check(x))
 check(no(x)) -> no(x)

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {7,6,5,4,3}
   transitions:
    up1(9) -> 10*
    up1(46) -> 47*
    up1(36) -> 37*
    up1(26) -> 27*
    check1(45) -> 46*
    check1(48) -> 49*
    no1(35) -> 36*
    no1(38) -> 39*
    sent1(25) -> 26*
    sent1(28) -> 29*
    sent1(8) -> 9*
    rec1(16) -> 17*
    rec1(18) -> 19*
    bot1() -> 8*
    rec0(2) -> 3*
    rec0(1) -> 3*
    sent0(2) -> 4*
    sent0(1) -> 4*
    no0(2) -> 5*
    no0(1) -> 5*
    bot0() -> 1*
    up0(2) -> 2*
    up0(1) -> 2*
    top0(2) -> 6*
    top0(1) -> 6*
    check0(2) -> 7*
    check0(1) -> 7*
    1 -> 48,38,28,18
    2 -> 45,35,25,16
    10 -> 17,19,9,3
    17 -> 9*
    19 -> 9*
    27 -> 26,4
    29 -> 26*
    37 -> 36,5
    39 -> 36*
    47 -> 46,7
    49 -> 46*
  problem:
   
  Qed